package com.opNaga.nusmvHelper;

import java.io.BufferedReader;
import java.io.File;
import java.io.InputStreamReader;
import java.util.LinkedList;
import java.util.List;

/**
 * User: Junyi BEI
 * Date: 08/02/2012
 * Time: 15:35
 */
public class NuSMVHelper {
  public static String runNuSMV() {
    String out = "";
    if(OS.isMac()) {
      String[] cmd = {"./bin/mac_os_x/NuSMV_2.5.4_Mac_OS_X", "help"};
      try {
        Process process = Runtime.getRuntime().exec(cmd);
        String s;
        BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(process.getInputStream()));
        while((s = bufferedReader.readLine()) != null) {
          out += s;
        }
        process.waitFor();
      } catch(Exception e) {
        e.printStackTrace();
      }
    } else if(OS.isWindows()) {
      String[] cmd = {"./bin/windows/NuSMV_2.5.4_Windows_x64.exe", "help"};
      try {
        Process process = Runtime.getRuntime().exec(cmd);
        String s;
        BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(process.getInputStream()));
        while((s = bufferedReader.readLine()) != null) {
          out += s;
        }
        process.waitFor();
      } catch(Exception e) {
        e.printStackTrace();
      }
    } else if(OS.isLinux()) {

    }
    return out;
  }

  public static String runNuSMV(String fileName, int bound) {
    String out = "";
    if(OS.isMac()) {
      String[] cmd = {"./bin/mac_os_x/NuSMV_2.5.4_Mac_OS_X", "-bmc", "-bmc_length", Integer.toString(bound), fileName};
      try {
        Process process = Runtime.getRuntime().exec(cmd);
        String s;
        BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(process.getInputStream()));
        while((s = bufferedReader.readLine()) != null) {
          out += s + "\n";
        }
        process.waitFor();
      } catch(Exception e) {
        e.printStackTrace();
      }
    } else if(OS.isWindows()) {
      String[] cmd = {"./bin/windows/NuSMV_2.5.4_Windows_x64.exe", "-bmc", "-bmc_length", Integer.toString(bound), fileName};
      try {
        Process process = Runtime.getRuntime().exec(cmd);
        String s;
        BufferedReader bufferedReader = new BufferedReader(new InputStreamReader(process.getInputStream()));
        while((s = bufferedReader.readLine()) != null) {
          out += s + "\n";
        }
        process.waitFor();
      } catch(Exception e) {
        e.printStackTrace();
      }
    } else if(OS.isLinux()) {

    }
    return out;
  }

  public static String runNuSMV(File file, int bound) {
    return runNuSMV(file.getAbsolutePath(), bound);
  }

  public static List<String> readOutput(String out) {
    LinkedList<String> ret = new LinkedList<String>();
    int traceStart = out.indexOf("Trace Description: BMC Counterexample");
    if(traceStart > 0) {
      String[] lines = out.substring(traceStart).split("\n");
      for(String line : lines) {
        line = line.trim().replaceAll(" ", "");
        String[] varEqualsBoolean = line.split("=");
        if(varEqualsBoolean.length < 2) {
          continue;
        }
        if(varEqualsBoolean[1].equals("TRUE")) {
          ret.addLast(varEqualsBoolean[0]);
        }
      }
    }
    return ret;
  }
}
